	Verifier behavior in RTL-Tokio and structure in Prolog	
	
		translator and facility-checker


Result ( filename : @* )

  @trans.out	:  the results of translation.

     Format

	predicate,ClauseId,Argument,Condition,NumberOfSubintval.

	state_call,CallingSubintId,CallingClock,CalledPredId,Argument.
	
	sub_int,SubintId,StopCond,MoreCond,Length.
	
	data_equal,SubintId,[Destination,Source],Clock.

	data_trans,SubintId,TransId,[Destination,ClockD],[Source,ClockS].

		PredId = (HeadName,Arity)
		ClauseId = [HeadName,Arity,ClauseNum]
		SubintId = [ClauseId,SubintNum]
		Destination,Source : [Op,T1,T2],[Op,T]	 operation
			             [*,Reg]		 register
				     [*,[Mem,Adr]]	 memory
		Clock : Time	    clock Time only
			(From,To)   all clocks from (beg + From) to (fin - To)

  @path		:  the process and result of facility check in a data_trans.

     Format

	SubintId

	---- process for searching paths  and 
		error message when data_path cannot implement a data_trans ----

	path,SubintId,Callers,TransId,UsingFacilities.

     Comment
	This TransId is equal to one of data_trans in @trans.out.
	The 'path' for same TransId is 'or'ed each other.

  @facility	:  the results of facility check in a sub_interval.

     Format

	facility,(SubintId,Callers),UsingFacilities.

	Error Message when conflict happens.

     Comment
	The 'facility' for same (SubintId,Callers) is 'or'ed each other.


Sample Program

	0test.tokio
		is suitable for facility checker.

	2test.tokio
		is suitable for time tracer.
